\begin{tabbing}
es{-}simul(${\it es}$;$e$;$j$;${\it ds}$;$s$.$P$($s$))
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=($\forall$$x$:Id. es{-}vartype(${\it es}$; $j$; $x$) $\subseteq$r fpf{-}cap(${\it ds}$;IdDeq;$x$;Top))\+
\\[0ex]c$\wedge$ \=(alle{-}at(${\it es}$;$j$;${\it e'}$.es{-}causl(${\it es}$; ${\it e'}$; $e$)\+
\\[0ex]$\Rightarrow$ \=($P$(es{-}state{-}after(${\it es}$;${\it e'}$))\+
\\[0ex]$\vee$ ($\exists$${\it e''}$:es{-}E(${\it es}$). (es{-}locl(${\it es}$; ${\it e'}$; ${\it e''}$) \& es{-}causl(${\it es}$; ${\it e'}$; $e$)))))
\-\\[0ex]\& \=alle{-}at(${\it es}$;$j$;${\it e'}$.es{-}causl(${\it es}$; $e$; ${\it e'}$)\+
\\[0ex]$\Rightarrow$ \=($P$(es{-}state{-}when(${\it es}$;${\it e'}$))\+
\\[0ex]$\vee$ ($\exists$${\it e''}$:es{-}E(${\it es}$). (es{-}locl(${\it es}$; ${\it e''}$; ${\it e'}$) \& es{-}causl(${\it es}$; $e$; ${\it e'}$))))))
\-\-\-\-
\end{tabbing}